Nuprl Lemma : qsub_wf
11,40
postcript
pdf
r
,
s
:rationals. (
r
-
s
)
rationals
latex
Definitions
r
-
s
,
t
T
,
x
:
A
.
B
(
x
)
,
subtype(
S
;
T
)
Lemmas
rationals
wf
,
int
inc
rationals
,
qmul
wf
,
qadd
wf
origin
r,s:rationals. (r - s) 
rationals r,s:rationals. (r - s) rationals Tx:A. B(x)